■ Artificial Intelligent Froie3fc-*HI£ ani K.{T Computation renter Wenc &i--The Prcofsbcsker by Pail Abraham .... . ' • -January £&, ipol JiBSTMGS The Frt:cf'ih^tVi r er ifi £ heurle tic-ally tri«itei cCB^putai? pro- gram for checking ira^matita! proofs ? w.'.th tb* ftheairtrtE of text- tccvc pp^pffl &g it* ultimate e<*al, :ft tone frusta, from esa* P* cc "? step jrii-»n to it. a. *orT£sponJin£ negusn-e of fcrrai Etepe, if pc.adibla. H peaor&a tha current ttate of the prcof in fcha forra of itfat It -56 s=uTJ.'JiJ.en*. tc prtve. There are two Logical Pul*S rf iaferenaa; »c*™ power* and iisasrlion (if it i* sufficient to prove P N 5^ A i*. a liheorein, tlien it is sufficient to prove A iiip^es F)* The peuniBPible fnvwai Ptepa ■■.rilJde these rules of infer eu-e as weii as provision fci hawSling definitions, icnaa, cB-l^tiiatlons, and revision ec previous state?. A? of now, mast of the fortnalipnt, o.?i* pjcsr&wip»3 an* partially debugged, bat the heurlatle &Epe-;tr have yet tc. be pro^raimnii* * v ■£<- TABLE OF CCNTEKIS i ?utpofe arid pttLloAaphy ■ * * * * * r * *' * ' " II OffsanasatJon of the ?rcof checker 7 III Logical Po-JErfatloBB of the Proof rtwdur - * • * ■ 13 IV Th* Poasitl* Froor S:;e*s in th-s Proof eh#a«ep - - 1? 7 Current Sfcatug and Future Plans 3 PI -3- ^JUPOSE AND PHILOSCPHI A proofs heeler la a computer program v:hlch checks watheriiatical proof* to- eeo if they ars correal;, k TnatheEr-atJ ral proof is a sym- bolic express! on f antf ao can be used aa input data for a "f^rnpitsr program vjritfcan in a syuibol-Gr.a.nipul&tlng l&nguage , Now if a proposed £roof has been sufficiently formalized, it can be the aired by a n*mple set of rules j but if che proof is of the sort that appears in most mathematics textbooks t the checking pro^c-dsra siyat be ft* Irene 3 y elaborate and even then cannot be guaranteed to worfc all the time.: Crhfi~! r .ino; textbook proofs ia the ultimate goal of tne Proof checker project, even thoarh it pirobably will not be reached, this goal Mli est [>hs direct if n of thete effort?-; how fa>? they go rentf'ns to be seen* Some programs have already been ch-C-kid out; rrttiiy regain to be written* ha of this writing two el^w^fjfcft^y formal "proofs h.ive been chocked.: h n -inter of the ideas presumed in this paper arose from suggestions made by £ohn McCarthy? however., the vIoyIhj expressed hoi.-e are not ne-ieesarily in a^re e [Dent v/ith McCarthy's., ?herc are two difficulties that arise in demising a procedure for checking ccjctbooln p-rcofiK First, the proof 3. are written in English \ se-eorjd, they ars ambiguous, inforital, and .full of gapGr I am not at present planning to deal with the first problem? though it 1b interesting, it is irrelevant to the main purpose of the Proof checks project* Therefore, 1 will afisutw that the proofs ;:hi.ch I wild like the Proof checker to sparine Mill be presented in a foraialised and stylised language, but one which makes no attempt? to clarify the logical defects of the English original from which thej are taken* The Pyoof^hej^er will have to correct these defects and check the resulting formal proof at the aame time* Essentially* the Proof ohec iter works by talcing each step that it it given and gens rating fror it a aequense or formal steps L Thus the proof given to it really serve a as a set: of hints on how to construct a formal pre of of the theorem at hand. The Proof- checker tnurt be something of a proof inventory t&v it mu&t among -it- ■ ■ , other things be able lo handle strips labelled as "obvlouo*. As the capabilities of the Proof checker increase, It i?il 1 got better and toot tor at proving nen theorem In fact, we ttay view the job of the Pi?oof checker to be to invent proofs, given a est of hints: in the two extreme capes, the hlnta ara either nonexistent or are all the utepe of a rorm&'L issd proof.. l.'e may consider tha problem from the viewpoint cf checking :iEthorta for gene rat ins proofs, lie., seeing; if a proposed Fi*?thod of proof generation gsnevatas a p^'oof of a desired theorem. Tha two viewpoint** are equivalent; tw a technique which will utilire Mnt? is 5irzply a proof Generator with an jnput., Further, tha Proof checker H-isfc be able to bkl!£3 use of information on ehat the (ceDbsia of a cai'. af.n c^a=;? of goalie expressions are legitimate proofs Such a piece of InVori-^ilon is a n-eta theorem, In order for any proof -checking ay stem to lit i lice rcetefchsorems, they ia<ist bo built Into its etr J:?tiire^ fn the Proof checker , rce t a theorems ciay be adder! without- ?hans£r£ * h* overall pattern of operation? aarentij:,iy P they are added tc the list of perraiselble proof atepra f so thay they act like addltif^ai rules o^ inference (vhieh, inieod, they are U The Heuristic A pproach 311S ii elatgd Work The Froofcbeeker win make extensive use of heuristic methods ■:":;. ti.;-hi-.3qu^3 . "h:!e is rii-cfizsary became a a tr^.i T.'-.s.f.- r.'.'^-d 3-p-j,rch through tha space of ooruv-tctions between snese salve hints would in- volve an impossibly l*r£. amount of computation, One scheme which I hop± will be useful h?,e will be the ,: Oer.&rsl Problem Solving System ! ' of fleuc-11 and E .uz-tu This system has already been ured in solving problems in trjgonoraetry, ele inert try algebra, and logic. The chief feature of '.tie system is Its separation of probl&ra content from proMem- solving rechnJque * jtt mattes use of two principal heuristic a: meanF-erda ane^-ysls, which invo]vea knowing what rrsthods of attack a]? epproprjate to particular situations, and planning which iaveivea consideration of an abstraction of Che -5- ■ problem tt hand* Closely r^ated to the fanning heuristic 1& the heuristic of modele as Uf.ed by Oelorntsr.. TiIe he- i :iriEtic y for tfcs case of plane goetSiefcr:/ r involves drawing figures and checking there to pee what relationships hold between tarloup line aecnsntg, anglee , etc* There is a r>e&ei£flan:<e between the pole of hints- in the Proofchecker alftd the rely of advice in McCarthy r e Advice Tales r achem^ in each fere, hfj i^nt a DiaohJ.se to nahe use of pieces of information given to It r? rorj an external source in ord^r to so^ve a problew. In thr* case of . ty.a Proof checker* the structure of the *advi<V r Kiak^o it raucfc e.ifJer to rtct armies how tc use it t Problem ^tflains The * , roofchecrk , e-r will not he tied to any particular area of" [jia:--heinatics , although 1 espeit to work mainly on abstract algebra at fi:?Efc, Tjhe Proof checker* like the mat hcrcaM clan, is Interidel to bo a general -pLirprpe device* Her s. given problem doo&ln, it will have relevant thecreiae, heuiMsti£,s 4 a>id tiodel-mkinc rae cho- rd yfc. store;! in its ra^ory* Actually* it would be useful if the Pi?oof shocker could be aiiari: of ili_ the theo rents It had ever prove i n , though it udc,hi have le;sp ready a^eas to those from different dom^Inf., The difficulty here Is that thara ainply isn ! t enough took iii the cemputerj as things stand n^tt, for the addifcio-nal t^eor-ems. One poaalble ar^a ef application, thojgn ad wit ted ly soisewhat futuristic, is to bhc uftseiwut of lai-f* ey&t*e?fl* The present way that one checks r-uch a £;yst-5GJ to pee If St crorfre ia to p^e^ent it tilth a wide vsrie.fcy *>f inputs representing both typical and extreme taped, and see If the proper output results^ However, it often happens that thii ic^thoci simply dca&ii't ^or!^; the system falls under podes unanticipated combination cf circuraatari^ag which nswr 3i;Curred in the tes* •- af pe t One i/ey tc check out such a system, however, la to pi- eve that it" worlr^ « Such a proof 4 of course t would be inpoeeible for a hufcn to Construct fc*r a system of aven aSld coup laxity; but a machine night b* £bis to eonatm-t such a proof, iiFiinfl as h*n^s the £t scrip!: I on of tbs- functions and intondsd rao3e of operations i?f various floiaponan^a and subcomponents of tha syjifcett* And in a prcof atfcaEipt, one rci^h^ ccrae up a'th g.' cO'^^terexampI-3 ar.d pcssibi/ ev T e:i sii^jzeifc e rer^dy* -7- 'GitfAfflZA^TOH OF THE PROOF^'HECKER The Proof checker is organized 'nfco ti:e constellations of programs? Wo^hoe. and Verify. In a> Iltion to tho data interna] to these programs., Clwre if a list a? theorem, a 13 at of defi- nitions* and a J % *t o? ,lo£ltUiat3 prwif .*tep3, Tlw theorem list and definition li?it may be a treated with time. verify will accept a proposad fonral pr;of step and tietermins If it is correct i if ths 3 tap ie cornet, Verify will d:> ths necessary updating of fche state of the universe, Method will tie t ermine what th<2 next step should be; it will make its a of nhe hints given as input in finding this step. The steps tehich Verify Bill accept must be Jn Bb&ndsrdlzed form? thus , all of the heuristics ara in the province? of Method, though Verify will hurnJl: updating in such £. teay as to rea^e the- u.eo of hourie bice easy* The current stats of the proof 13 recorded in the form of what it is sufficient to p;?ovo* We will call this expression the CLifficiansy, i,e., at each stage It iu sufficient to piovs the ftufficlency* Then Ir/tially, tho sufficiency its the theorem wa uistt to prove; arei Nhen the sufficiency hsa been reduced to T {truth), we know vs have proved fchs theorem* Wb nay record the tuff icier cy at various stages of ths proof sncl refer bncif to it later, oo that If r,s conduct an unsuc easeful aubprobleBa exploration, ve :3an return to E.n earlier siabproblerc ivithznit havir.a to repeat the Initial stops of tbo proof* This particular foiw of recording - ne iurrent situation is con- venient because of the uids variety of logical s true fur as which may appear in a theorem or in it& p?ocf* "0 use a list of hypotheses and conclusions would ba aukw&rd, for instance, In handling an if- and -only- if thaorena, unless ilr were to be broken doe:n into two separate theorem* • Yet Eu^h theorem;? are often proved by a sequence of bi conditionals > and this natural sequence can be retained in the sufficiency forir-oiaticm of the proofs Further more, this formulation aaliK-a backwards proofs quite easy to handle, and they ara per hips the moat nature! kind, Afc the tf&iae time, It x is possible by using certain logical taut qloEi.es- to icake forward proofs; and the TqaC'tilnsry for hanlllng Such ^roofE oan b-2 fc.il Ifc into Mofchod irt sueh 4 WE.y that the u&er need not be a;sa.ve of the few complications that this entails- ■■ ■ • . ■ . . - . The Theodora Llet The Pro of checker in endowed with an initial get of theorems which are placed on a tli^orem 11a t„ ani each newly proved theorem Is added to this 15 at. t^mraas proved during the course of pravinE a theorem are also added to Ihis list. When-aver a theorem ia referred to In a proofs it. is btoucht to the head of the theorem list j so that frequently u^ed thacretifc are ennily ac c ass Ibis « Each theorem consists of a nam?, a list of variables t and £ forjtu Whenever the theorem is used In a proof, it Is referred to by narcsj the va^ifcibles designate those elen>snbs In the forci which lt.:^ b^ substituted for* We z?s.y think of the variables as designating an^.vei-sal iiutntlfiers which I implicitly precede the forra so as to convert It to a th^orew in the ordinary senao. The form is the actual statement of the theorss; no inhjarsnt res trl-t ions are placed upon its foriaat, though for any problem domain, the format will be specified. The Cefl r ltlon List The Proof che; Iter aim h&e available to it a list of definitions, A proof r.ay bs interrupted at amy point to raaUe a new definition* A definition is a Imply an abbreviation, with provision for sub- otltuting- for certain variables within it a Each definition consists, of two r-ames, a list of variables , and a form. The reference nacig Is U&&d when, we refer to the definition ir a proof step, and the Internal na^a is the one actually recorded in the sufficiency and in any theorems or. the theorem list in which the definition ia used^ The form ard variables operate in the sane way as the form and variables in £ theorem. DefinllimiS, like theorems, are arranged ao that recently used definitions appe&r at the head the list. ■ ■ ■ Th.-i Need for Two Faroes 1 We need two narca-B in a dof Jnltion because etheruiae we way accidentally assl^i to & definition a re revenue nrne whith already I133 a meaning; and then >y riiklr^ use of the definition, ws nay make e false atep »-:hith vrill p?>hf ^'r^rf-.U Ar, —iewdIs 7? ill illustrate fetis danger* jiftpMe now that we have cii]y one name aepioclafci;d wiC-h & definition* Let ue define AJ!D with varieties X and li as {NOT, (OR.. X ? V? > n Tbtia AKD iq the raws, Ol, Y) it the ;lrt of variables, and ()3GT, {HR r a, ")) is ths fory& T Sew uuppose Fiv^t ue h&ve as theorem (HOP, (OR. t, T)1, Shan ths theorem is the original s uff iciescy, By ualng the d«fini felon * we may then get a? sufficiency (AND, T. T); and by other Fjaara we loay reduce thin to !?, ThU3 ws HOUL(i have somehow prevented froti: entering the AJ3D Into the, Buffl&iency li! the above example, we would not have bean sblu to carry out the proof. If an Internal natsa- say GOOOJ, hat. been entered Jn p'.ise of AMD, we would have had as sufficiency {GoGO^, ?, ?), which won! id be unprovable a 3 nee GO003 hag no Vrr?:"^ propel tl^y d In jjensrLx.lj too u.i-e the raferencs n&i3ie when tie refer to & defi- nition in a proof, bv.b the internal n&ma it the one actually re^oi-der In the sufficiency. The Verify prcgrarc handles the "substitution of ■:ha internal nafl^ for th* reference mrae automat} eally,, Hhrr in- ternal EfiiKto ic a newly" ^enar^ted aym'jol which can be guaranteed not to have baen uaocJ for anything bsftre; the progrs-7?! which creates i:ur.h eynbola lit l£$& is c-ajled Usrioyn, The symbols, it gens re. tee are of the ft.ria Gxxxk, vrht.ra tha j: r s a^G d^cir.ial digits ^ Etedafinltion It 3a possible to redefine a term 5/tr. though. It ha& previously been defined, Itti-on ws cic thia t how-aver , vo lost the ability to refer to the previous definition, This is hacausa whar. me eearGh the definition JUrt for the reference riaise, wa will always come to th^ later deficit len fir&t; and ws can ae^e-."^ a definition in a proof step only through, ite reference name^ This le as one wo aid :ika It to bai for St permits -^ to- make teTRporary definition? -3.0- of tense: without presr^diia ths later us?e of ths^e tortus for othar purposes. The interna; 1 . r.aiTi^r of tho auctee-alvB definitions will remain tniquey £o thr*re la no 3«n£er of ronfislori, Often, f.n a he uric tin proof, tfe toil J Bake steps tshloh, rihila correct, don't help to prove the Lheo^eig. Sir±«e sueh steps may actually lead us to a r} tuition uhere ths suffis'^ncy la a fal- sity {&r*d he/ite t&iprovafcle ) , we emefc have a May to e° bash to pr-evtoiia suf fiajenoies.. At th*? same- tljae^ wq ^o^ h t want to fcssep all previous Buffi^innujes, because it rjay talre up too igjoh rocra. Therefore, there are tifc ways in which we nay nave past sufficiencies.. BevertiRg YJhen We il£tre a "tap, *ie nay request that tfc-j ^ast sufficiency be preserved^ V't ns; 17 gi-ln R<33 eg 5 to :S t t-y reverting one or more times, depending on how fp7 a] 0x45 va have Lioved subasfrjientlj . Tr.ere It a parameter^ set by Wa^hoA, which tella Verify whether or net to preserve ths most recant tuff ivis-nay, Tt.a list of FjL T e_a_ejryed- jkib problerciE. The reverting p^oc^dturji is no-: aj^uafce irhfcjj we wish to bail: up several step?*, move ciff in aiiothar direction, and then, after the r-ew exploration proves feasible, return to frh^re tje started. It 1e inadequate be^auflfc th* starting point lies on a different branih of the explorer Uw tree. ;{n order to handle this, there Is provision for naming the eurri-n!: sufficiency at any tlras find storing It on a list of auhproblero to be preserved. At any point,, we mey reattach it if we: *j±fih„ We may also r-cmeva any a off id en-.: y from the ltat of preserved QubptPOblenSr The items on the list or? preserved aubproblenfi are then aoceaiad by their narae . When tha theorem at hand h&a be*u proved, the list of preserved subproblems If eL-t-onaeic&lly Glfi&rad, -11- Ea*.-h tyi» or proof etcp Is 1 rap**j*ent*d bjr & program which taker ths parameters of the step as 'r.pul., updates Khatsye? needs to bfj u-jduttd, and £.-v^ at output" T or 1'. d op 3-; lino; on Heather or not she proof otap 1b correct. tfrtati (■■wis tr,sy toe incerpovatid into ttto system If they ire sat up a& pace of etepaj crdlnsrilyj they will tel:-s t;ie aaff.'^enay at as input , test it or a gutajt- ppeefllon of L.t for a Et&:*tiful£r prcptrty, ar^l rberi trEnafariE It in acta* uay L ]*q.' 2 list ante, £ 1o£I~el elc^lifijtUioR program would correspond t-o b jestathsoreEj ru;l"! a pro^sa racjj.d red^c the sufficiency to a ei;:^1#:? tuJ: logic ttlJv eq;uI T , ajLant- ibrci. The actual raatatheoron ts?uirt be £hat Mis rssi;!: of t-lmplification is *n a very case lo^jfc&Uy a^eivalsftfe to vha original, forra. ?»- j- V' erj.fy ?| 1 oc;j^m Tb/i Verify vTrogr&S] . tp we hat;c po^n^.i out, ciitckB each successive ftsp of the proof, and perfoi^ui: various k^nda of up- dating* Before exEBSiiaine any eteps, it etijigns internal t:aro5£ fcc f..".1 the variables p.o as to avcad &onfXi<strr i-;Jth preuto-jsly aBPlgned Ckan?J^i: L Thereafter* when v^riLbl^a are referred -to fey their ffcK&F, Verify raplAasn 1;h#BS n£Pi33 with Lhj internal names jjn the eteps* of Hie proof., V;i-:e ir.iithtd nea-i no : e T jen be autare of the existence of thoce iriti"ijal ns^ee*. UFarllv also asts tha 3Jfficic;niy inJilall.y to bo zht theorem wt v:ieh to prt^i; wh^n thfi khsorarn h^a been proved , V*fify pln.cfc- it s.t the hear? t>£ the theorem list. Verify repeatedly calls on Hstho-l to ppodL.'.e a prcof etep fl Each pt-ooi" slop it in-Heated b*y the r-fi" 1 ^ of a p;^£rari> sr.d- a get of argu- ments for tht,t p?cgr&n; , Verify ^hacliP fchf\ tfro prograra nairis i& on the list of iGgljjircaiVe proof jstepa, and, jf so, cjp^rat^s t;]i^ pro- eraoii ?ha ri:Suli; irKj3.T;:tes whether or not the step was o/orreit; the proof tU-.p pro&rara ]]andlen the up^citir^ th*it needa t-o be done.- -IS- . T]i3 Method ProfTafn Wet hod 1? called iipon repeatedly by Verify tc furnish pre of steps.. IfJhlle Verify will prob&bly reirj.ln unfihin^d £S the Proof - oheclcer is piodHfiefl, itat'.-ujd iciii be highly rubiest to chants. Method us as hecriatj.c isathods, in general, to determine what the next proof atop should be. At present, Hetfrod air.rjly feed* the . Input directly tc Verify, but this is onijr in order to check out Vsrify, As wrar-k progresses * Kathod will bscoBia ttore and Lr L o?e elaborate , Qna possible way of elaborating Method it to 3o to hierar- ofri^ally, R^thsi 1 then reh"?5.t£ Ketlt?i tc acoounfc for hsw lnprow- casnts* t new Method would by written which uses the ojd ons as a subpposrrii?. This technique is well adapted %a heuristic progparas. F tela of Condon g u'o g* pr J s 3 i_or g In eucesseiv* sufficienc-is^ there will often be Urge sub- expr&SBio:rjE which &*£■ carried elc-ng intact and er j j therefore idsnticalr The Proofcheo'icer ha? b^en tr girt:, zed £o aa to have both sufficiencies refer to fcha sai*i2 ropy ^f such a subexpression. In gonRral, copying is t^oidil as much a» possible, stvlns storage and time* Tuis might appear to bs merely a pracsirjai programming device t but it has an interact ins counterpart In ta;^booV cia the mat led . Ea^antially, ccrarson pubeipraoetons not like pron.o^inc; thny are useful in the sajoe way that it is useful in a boo.c to write an equation, nurab=r it, ana later on refer to i.t by number. If mo did not use the numbering techniqje op its equivalent, rfe would have to write the equf-tion out in fun whenaTsr we wanted to refer to it. • -13- LOGlCftL FOljmtfiTKHS OF TEE PR Vs will etart with £ siaes or pairs ^j*^) for * = £/ £ # - - i which we shall call Iftifrlal tLeargflg » K&eh T i is a ayutoolic «.- preE£lon;ea<:b B^ is a £«t af at^TJ-fl Eymtols ctr^Mia* l "* '^In J V* refer to ^ &i? th? fcjriL of ttiie theorem arrt to '.hec^, as the vs .frii.tles of the thsoran*. .tf jj ^ P ■_ 2 P *♦- r u-^ are eyrc-boli-i ex- pi-ei»t:ionp, than the result of putytitJting ^^ for^i^u^ for ^g* ,.• , u ]c forct^j, Jn ^ iB a theorem i nat&nge . Kt-i L e that the T^ ■ k are thtiorera- ine-Kinces ty the jfl^n-ifcy substitution. A proper tyl^cs gyaftol is att sialic symbol l?hl£t is used solely sr a variable in a theo-rer, and for no o-'her purpose, For inatancft, &10 and PSAISE woxld not be proftrfcylese symbols* In LIS?, the function GEK3YM In used tc triage these symbols. Ie~ 5_ bs a symbolic axprc&n? on, and HippofiQ 1:hafc there exists a fl^juenoe of sent elites S,, 3 2 , -,• , S n F-^ch that 5^ — S 4 /;. = 1 , 2. , -. , n) and ^ is the eyntol ,: T'\ (The neonlng of *-* will be explain .2d shortly; T reprttents troth.) Ish p^PU, •>« > & m be * fli:t of prop«rt^lee£ sy^jole, tnd danote thlG set ty^. Than 1 ha p^lr i&-, r V) i- a nLeorem P-jrthsrn^re^ the initial theorems are theoz-nin;- * The class of thsoz'eire if tKjs forced recursively, tarring with the initial theorems. We 6eaot,& "i" ia a trhsorent inKs^e' 1 by - s.« an J tt it is sufficient to pro re P'" ty *"J 3., The logical ays'eni IB baRfcd on *:wq: riles of Inference* 1. If h T and -t S, then -i T"iS. f Insertion rale) 3, If t-5^5 1 and -fS*,, Mien H?. (Modus, ponens ) ■ - A - ■ jnt.-'j.it^ftjy* £ ~- F [ m*ann -f S ^ -/P 1 . Formally tte say S,«- S [ if and onlj- if ■" - L S ! lis of the form Tr*. 1 ? and f- T, fir •:.«-. E, /* S l :??, or J, S' 1b obtained froTi S by substituting for foms eabex- prappion of S the equl-Yr,lsnt of that &jb express ion, provided that the auto evp re Eaton la ; L *ot part cf a quoted eubejcpreasion, Eo^ vacant subexpressions are of twa types; 1* ft def Inad tenn la 5 qui v slant to thai; Khith It def< naa« £« An exproaeioii i.;hich r spree gli^ tha raeaiL: of a calculation IP eq\A5, volant to the : ii e&ult itself." Fhe calculation ie p9rfoi*Ji£d F;y evaluating the expression ajad then replacing it by the quoted reauit of the eva^uat^on. For instance, ttoiQd be equivalent to (QUOTE, £CGH3, (?, [A, B)})* Here £UB#T 1e a LIS? function which sjh6titu*:ss its first EirfciM&nS for Itc second ar^upgnt :ln lb 9 third argura-irit r 1:he lefinltior; of — 3 a .? hanged vjberi, mfrtatlisarsTrE are .added to ^h<j sjietufj-i Eherafcre, ;he above description corresponds to the »y&feera arc it now s^a-i^da, but in ry»t perifoarxiRC T Role cf Initial T'.^'sorece ■■■Tie initial theorems differ from ejeioras as we think of thew In thfifc Cor H^st preplan, detains fchere is no effort to snake t-hei.i non-rodu^dint ^ By ual^g a system wjtli a lar^e initial endowment, iri;.ej?rj5t!.ng result: 1, sra raa/hed more c nicely. It Is true that all of esa'jhe natlca may bis constructed from lower predicate calculnc with identity; bat the working Gathe3tf.ti.cian clcss not ordinarily ral^e lee of bills fiLf;t, even tho^n he la aware of it* This is as true -."or t^po„ogla.bs arid algebralaleU. as it is for hyvSrodyr^mi^iet* ar.1 nimri-ml analysts, even though the former may occasionally give This page is missing from the original document. -16- h,; he Varmnt of the? Calc ilstl^n R^e In psr-crj.UUiR t*e cuictij atiari r-.il 9 r we have 1st the wolf in the door. Wo voulA life trhs Froof^haslcer, when g*ven a proof, to te fuarfikTitaed to ^.vt? ui ft vordiit- However, whan wo j.hfcrodus* t-hfe G&lGUl&tiior! r-:;.e, t--J cefl. rto ledger guarantee this, except at great coE-t. FG* whsm w-i ceietrt acme gutsxpreaaion of the sufficiency ar^ci proceed to da:- f-iilct a iia v&lu*, fcii& ealiiiliitlori ir-ay rot ter- crtiAte; furthermore p U f.B in ffjrt'rAl '.K^r»e?ibl^ it protest the sut express ion to see ^hethir r-r r.ol liie eal^ulafclcn t.ill r-n wild ?r: aors X&T.B& art;? d^f/fr^ t'-.t; Proof r^n^e* 1 prc-gratf or r,c?Jify its sonkents , {A fantastically ^lcvar j.aarj:ir<£ prcsraw, for infrtante, iiwcht ie;irn to eh*iat by tnodifylng she p&rai&iesGrs of the Proof - -he-L^er do &? tc Tot'-s i'r to asso^ fal r .s ^epai; J iho»-i problem may be skived by running all s&I-rolatleK steps «i fin Interpretive b'arSs, bat this requires a yrl /&.te and <juite elaboraU interr*eisr Per tke ?roofchca;jst»j fu^tl«eru!ore, it w^uld be jJHfco&Fa£ly !rip*e*- consuming because i3B.ahin.*-i&ng , 'irLfre progrSiaE at t*&l^ EJ9 higher- ^e*'5;i-- ! a:'j ( g-j££ J r£ J ' praj.;:^^ '-.oiiid h£"t; te bo interpreted r ?hi:* diffiri-jity la ;-:&r*died by placing ail calculations imdor the control ^: a program rat'ert Errorccr... Errn^et causes meat; detected errwffts and .'.orj- ! eppiJnatli^ c&ic-jiatieh* to return to con- trol to 1 -ha Fx i aafiihettfc'7r . It raili net £?it-V(i an pu;:t, arrorf*; so ;h:l.g loslstl jLoapbaln do?? rsrta:n, Eowysr, defective proofs Khlah do get by Error 35 1 tflil ardi nar3 iy c£P5& Hie ?»&■*> fuhtM^er to 6 top richer t^an to ?£v-5 & fa~'?.3 ail^Y^r. ■i;- TSSJ& POCKVX-Iii S'ltFS IS Tii'i raOOFCilHSTJES Wrien Verify rs^e-Sv^s a proof step flora Method, it checks to sea if th* step Ss of on? c? th& rsict|."C«^ tvt , ^i J &^G has the appropriate svitfr-er of parage 1 , ctt ^li:-h 5 t . If" rat , *he step *e erron'aaus, If thece ?:i3tai*ia a?a j&ef;, t > : & ti^re o:* Vr-.c i:-,ep ie fasten as the r.^irt of ft fjan£iJLcn, a.nd Mna pir&iT^t&PS of the c,:&p as avgiunsjnt? Pf U-.^t Fuiw.fclott- fot- ei! , >r hypo of step f she jorKv- Erp^hdlRg F'.ino 4 '* on LV}ic-. n it? the !?-tcu ».c foe i.f f it \G .■ , :0.. , ?'3.;t Ahd, ii £lv, £■?-£;■ tha jw-s^ssery updating 1'r c function i? tfuleti by Verify,. The typas of prf.rf ^tspF have tet.'?. e <j Ler.teci fer rJie.'.r uris- fulness a? pf!miri<;ot : - or* bit-LId^ng-blc^lts is coiiatfjtfv.ifijv T-he r:yp*:£ of r 4 . sp* w are rea.^y 5 1*^ row ted ift. Th*? £*$; r&ol all ueefa2 by fr.be pp a?, vet? . t*- v, eve _*■ , v> ; « -, ^. & i i xi £ l-c jpr a .id -lX; fcfc 3 n i d hI tl: r^e r ta I ft ffpa?4flr theoreiffi, rtty bj'jol-5 =jui":E ptf-tsrilll. The- fc;:ir>tffa# step.* art a¥ai}.B*Xa a* freyeut; tiii ti pl'ep lass a? par sine ?>arc She n&ws of -a theorem and a 1 5 k i r.f p i A h t *. ? i* c i c na . T he c or \ ■■& s po r*3 ! ng f utu* ti o^ finds t>>e theorea on the theorem D.J'-S - . perfc-rras. the i ind icat e d ?, abn i i t u£ i t n"? . and t h en app 15 m t ! "ii - ^r a v t if: r, suie io the resulting. xhaor*i3 lr.jnan:o a^»1 tfca curr^n;; ft uf fide-nay. if tha n?ise(3 tb&orein r,s wo 5 on the* thsoren Ii.et, or if th«; variatifts r .r- fciw etiibstlt it'^cri r-i*'t do not corre^-jO'M ' z.- t'cs :^r- i*5j.s:.. c? X'r.s C'.eotcin, the step is redacted, l^^s e^^p h£.a t." parameter tin-. naiEa of s theorem* The correspcnii^JiE f^msticn flr.-i^ tl-.e Theorem on &hs thaorais li-ft, ^etermjnea iht px-npei EJbititutiOTW for th& Var^sait'S tf tl*e L^eorena,, p.n:l v ,h.?i sppii^s ttj& r^it of r'ttt'BrAB -ipiup ponena i-o t?ie ;'-e iUlt ;.n^ theorsrn ard the i ui re n f, & ■. if f i .4 :: eh; j? k Th ^ ■-- \ & x ■■ -.-■ \. i ;-. b:» ?v- jes t=ed If 1 1 o nutae'd ^n?orere ;' ■? nor f^n :i e '^-eoresr. H?t, cr if t.!i* ther-.^ rtf- t/.r. nat c.f the f'pr.i (Ih'ME?, antecedent, eonsffrijent 3 , or If She sufficiency "* no* a fi Jibuti tut ion i*istan.%e of the' nonsequent with reject to tha varieties of '-he theorem . ■?hla step faa a* arg'itier.fc & lt*t cT A's art4 D ; a tfMsfc indicate the. a ufc s K.pr e * rr .1 en of fcfro c i-f t* J - c lc *>;* y ft her e va > ije is to be calc^atsS. If the i;.Fb Y.&h r,o alMfehia, the F'jbexprefisiori is the entirs entprsfcsicn* T^ie rt-?p rap"ia*i»G the nubexprevfiScin * ty Li at (QHCTE; #val[/]l* The &fcep will be re Jet to-:! if the list reaches nu ascitic symbol c>i H a quoted exprtt-sicr, po?c;'<» :; ^ &\hi;-;y ;.<M . Mr.is step hat af- QrjTMLnjiit^ & na-^ r a 1'tl of ■,■ ariaV Isj ± and a form. »?i th.f. =s ?^pp T t.'oe ?roc^cher-.ker in used recuPfi'velTj £o eh^u the proof of a lemgta, ahil? ^ erupt - rarily neglecting L.fce? main tr^crem, XV rhe APin^a ia proven ; it le added to the zfczor&u list; in eny caae T t oc- troi 1? ret-iFTW!- to the prccf of '.he Ttsain theorstf wh*f: either the ieaac-s ia proven or th? r -r oof ghee !/er ia is 16 to giv* y$j m it, 5, M&kedEf Thi.3 Siep haa as ar^Juanttt a nams, a list of variables, an^ a for©. The sorrespenaing fono#ion firs', assign? an interna^ nzuae to be th-3 equivalent or the TT& France ri£it:e. It then pla.ics the list which contalna bo^.h nsnsss, the variables, , ejfot the for** at tr.e begjLnnin,^ of U"j*s tff fir,' t:. Oil 116 1- Thir. Siiftp Ivf.i* af parsmster^ s, r.anrs ani a Hit- of A -a ani D'ji„ Ths A l 4 F4^ D's ar£ ur.e:l r,o indicate a Ruhej.- pref.ft5.on of the &uf£loIejrKj7: the name ^a Vhe re f trance narje «r a i^firjl.tior, . ?'!"■«■ a-orre^j^nii^^ ^unotien ^e^i i!e 3e'fir.it1rs:i frnm J-.h? i*firj;icn ii*v a^.? cha^ir t-.ft* ■j-.ilr-exTjref'.sicri to ree if i. :3^ & iat:-;it,jtion intt.pr.-fl of 19 the fann of the de fin iti on< It 1 ?"^ it t-c-;-j ;i;aa sh* sut- ejpression by ti llss nfoose first alftjaar^ i« rhe interna'- narao- of the definite ce, ?h^ remitting elements haire the property that ;,f thoy are maiihed sequentially with the variables or ?.he difinlfc'on ami nuLft<u&M for ther*e variables 1'^ the forw, the result Ifl the original subexpression.. T* yn-Je f * no Th', P E-.op hf.k as paries!;, er a 11 it cnf A F E anl r c & Hhigh indicate e. sutcjipres^^rj of the ciffieiefisy* The first el^Btar-fc of this :i:;!l.e:':p:r5B'iiar[ i^ t&'Ken a# the !/■- terra! nacre o" a defini titn, an;t che definition list is bsarehed for ^at naore. a oatatAsution llFt* is fora,-?d by na tubing thf- euacesaive alercents of Bhe subexpression with T-bs v£riabze:i cf the definition^ an 2 then the indioal-ed a , jfcst,s.t ation* ors performed on tbo forra of th-j definition,. P:.nally J the 5 Un Repression \c. replaced by the result of this substitution. Ehe step is Fixated if the naKe^l d^fiuitioa i* not &n the definition list, or if the number =f e!i agents foMo^'.rj^ the internal name of She "tef'n.V^ott in 1-ht ^-iiic-yp:e j >fien Ts-nat a^ual to the njr.ibor of \&.rifctlt:3 ci' r^ euberpre salon. Th; 1 -j **>ep haE af ^r;; no '. 5T & reference naine . It causes *-: pair fhees fi?rt oleisent is, the na-w and Nftose Teccrrf els-^n', i* t?.«e a arrant- sufficiency to le pla^d an the list of prefe-srved JEUVprfltlCMl, The aurrent BaffieietK? wll] he- aMe to be itohvOt-.sj .Vf n^i e^E^ry a 1 ; a later tiTis-. 9. fiea t_t!i^;j![ "h.^s step has a?, parameter ttie raraa of a 5 ^bprofclera on ih« lis? of preserved &ubpret lecig- ■ X~ causes the current auff'iclensy to te ->et to tbe- & L jf fiaien^y psire-3 -20- wlth bhe gi.vari nana on (h* Ms 1, of prt'atrvecl nu^praMeas.. Eh? Etep is r£js<i:^c-rl XT the naius <5ois imt cor-Fo-spojvl ic a Tiiia ;jf.?p har- at pa 7 ir,:c-l,ei" the iniue of a prokl?m 01; the list of prefer ved su'.-prfti.leJHS . ICt ea;j.£i?£ that s-Jb- pjroblem tD bs csje'ied frcr- the Iijt v 11, jp-j nath^ g ^riift Et;en has nc parsi^ters, .and has ito effect fchatsotrer h IE. geygrt ?b*p r.i ep ha^ nfl parar.L aer*£ . It cfcUf.en as to take tir.fr aer-OMi nott recent. &uff,1.( J.-e.r;Cy a*? thy Current eufficiewy* If tte ruirent sufficiency if the theorem we wish tr prove, Uj-> step If.-. itst j^steeK Ifoleis the current &ufflcisrjjj it? sived ty a riE.mepr>: f a revert trill C2 l ^-e it to be Loefci *£hi& ?iie|i has n^ par&rae^erft. ."Lf the ejrrsnfc s.tfflfi&n^y 1e "T", u* place the th&wea .if, the It's* A of the theorem llstj Rnd Voril'y will return with Lrt ans"*? of Ti If tihe eufflalenoy 3p r^t- 7 r t-hfc s-.ep 2 s rejected. ... &&&E3¥2 STATUS WD FBT-JRJ; PLA'W : -^'-i llf of this writing, the Verify p-rot.ran is In the process a J' debugging, and the- PfeShod program i* in ifce ime' riwli merit ary fornj . Kethnd merely tfekes a List of alepe, peel* them off one by one, and pfifses than to Verify, while print irig o^i; useful lnfonEition. the ppogrram has teen co3#3 entirely ir: MSF, which seems to te well suited (re the appjieaMon. Jr: pi&irtirtii&r, ifca handling of i^otaaon subesprep^onp without raneiie&s&r; dupi* cation will probably ease the storage difficulties .lonaideraLly when the praMava get nk^re complicated and the t-rieor;^ &rA definition lists £a^ longer, ji have already wriev-er. all the functiona which eheok trie differ*: sit. ftepL', though - c :cne cf t iir-n sr;; in <jee3 c f revision, After Verify fcJ 3 its satellite functions have bse.ii chs.--ked o'j^ .1 paan Tic wcrW 02: improving Re«hod, at the same tiins applying It to ehsrtra^t. aisahrii,. Ky fi^s', c'.e-. will be t-c incorporate nstiiro-Fteps which Hi. 11 ccrnHne several infiivJducJ atepe along with gpeniftj ttsQreii^ . ^kr>. t 1 £h-;ll bulla * n sac hi nary i»;hlcb allo^'t t rjs a "r.e p*j !: £ t e p cine .■;■? m ti a ;?"."- l£ ■ io .1*3 ^.y ill ve n> *-f or "1 np " & jv e ? the £ '.Lb - Htit-jt.Jona ttJght. he omitted faa 1^ ofler, dotrc ir, ths oi tat ion of a theorem in a le>. thesis ^ronf}. After that, I shall investigate various learning itierhi*r.iffiDS whi.?h raij=h^ be incorporated- ' However, 1* ia difficult ta anUsipate a 4 : this point Just what cojra-? the projsei will foin&w; fh-a plan,* at cash stag* will be infl^en^ed sr-rsngiy fcy the rOP^Jti* of t-hu pr&ce'3in£ f.taee. ■